%Made in Laski
\begin{problema}{palabrasRecurrentesT}{t: Trivia, n: \ent}{[String]}
	\asegura{(\longitud{result}==0) \implica (\neg(\exists p \selec
	palabrasTrivia(t)) \longitud {p} \geq n)}
	\asegura[noSobran]{(\forall j \selec result) masUsada(j,t,n)}
	\asegura[noFaltan]{(\forall j \selec palabrasTrivia(t), masUsada(j,t,n)) j \in result }
	\asegura{sinRepetidos(result)}
\end{problema}	

	\medskip
	
	\begin{aux}{masUsada}{j: String, t: Trivia, n: \ent}{Bool}{\\
		\longitud {j} \geq n \ylogico
		(\forall p \selec palabrasTrivia(t), \longitud {p} \geq n)aparicionesT(j,t) \geq aparicionesT(p,t)
	}
	\end{aux}
	
	\begin{aux}{aparicionesT}{j: String, t: Trivia}{\ent}{
		cuenta(j,palabrasTrivia(t))}
	\end{aux}
		
	\begin{aux}{PalabrasTrivia}{t:Trivia}{[String]}{damePalabras(dameTextoCrudoT(t))}
	\end{aux}
	
	
	\begin{aux}{dameTextoCrudoT}{t: Trivia}{String}{
		\concat ( \comp{ texto(p) \masmas ''\ \ '' \masmas rtaCorrecta(p) \masmas ''\ \
		''}{p \selec preguntas(t)}) }
	\end{aux}
	
	% Aprobado por Lea Domingo 25 de Septiembre pero Duda. Anda bien el Scope de
	% los 2 asegura que usan 'j' como variable ?? xD, jam�s voy a entender qu� es
	% el Scope.
	